implies2(not1(x), y) -> or2(x, y)
implies2(not1(x), or2(y, z)) -> implies2(y, or2(x, z))
implies2(x, or2(y, z)) -> or2(y, implies2(x, z))
↳ QTRS
↳ DependencyPairsProof
implies2(not1(x), y) -> or2(x, y)
implies2(not1(x), or2(y, z)) -> implies2(y, or2(x, z))
implies2(x, or2(y, z)) -> or2(y, implies2(x, z))
IMPLIES2(x, or2(y, z)) -> IMPLIES2(x, z)
IMPLIES2(not1(x), or2(y, z)) -> IMPLIES2(y, or2(x, z))
implies2(not1(x), y) -> or2(x, y)
implies2(not1(x), or2(y, z)) -> implies2(y, or2(x, z))
implies2(x, or2(y, z)) -> or2(y, implies2(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
IMPLIES2(x, or2(y, z)) -> IMPLIES2(x, z)
IMPLIES2(not1(x), or2(y, z)) -> IMPLIES2(y, or2(x, z))
implies2(not1(x), y) -> or2(x, y)
implies2(not1(x), or2(y, z)) -> implies2(y, or2(x, z))
implies2(x, or2(y, z)) -> or2(y, implies2(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IMPLIES2(x, or2(y, z)) -> IMPLIES2(x, z)
Used ordering: Polynomial Order [17,21] with Interpretation:
IMPLIES2(not1(x), or2(y, z)) -> IMPLIES2(y, or2(x, z))
POL( IMPLIES2(x1, x2) ) = max{0, x2 - 2}
POL( or2(x1, x2) ) = x2 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
IMPLIES2(not1(x), or2(y, z)) -> IMPLIES2(y, or2(x, z))
implies2(not1(x), y) -> or2(x, y)
implies2(not1(x), or2(y, z)) -> implies2(y, or2(x, z))
implies2(x, or2(y, z)) -> or2(y, implies2(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IMPLIES2(not1(x), or2(y, z)) -> IMPLIES2(y, or2(x, z))
POL( IMPLIES2(x1, x2) ) = max{0, x1 + x2 - 3}
POL( not1(x1) ) = x1 + 1
POL( or2(x1, x2) ) = x1 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
implies2(not1(x), y) -> or2(x, y)
implies2(not1(x), or2(y, z)) -> implies2(y, or2(x, z))
implies2(x, or2(y, z)) -> or2(y, implies2(x, z))